EqDecider(T) == eq:(TT)  (x,y:T. (x = y)  ((eq(x,y)))) 

latex

---

clarification:

EqDecider(T) == eq:(TT)  (x:T, y:T. (x = y  T)  ((eq(x,y)))) 

latex

Definitions	x:A  B(x), x:AB(x), , x:A. B(x), P  Q, s = t, b, f(a)
FDL editor aliases	deq